Consequence Finding in Modal Logic [PhD Thesis]

1 Introduction 1
2 The Modal Logic Kn 11
2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3 Logical Consequence . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.4 Basic Transformations . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.5 Basic Reasoning Tasks . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.6 Uniform Interpolation . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.7 Relation to First-Order Logic . . . . . . . . . . . . . . . . . . . . . . 41
2.8 Relation to Description Logics . . . . . . . . . . . . . . . . . . . . . . 42
2.8.1 A short introduction to description logics . . . . . . . . . . . 43
2.8.2 The description logic ALC . . . . . . . . . . . . . . . . . . . . 44
2.8.3 The description logic ALE . . . . . . . . . . . . . . . . . . . . 46
3 Prime Implicates and Prime Implicants in Kn 51
3.1 Defining Clauses and Terms in Kn . . . . . . . . . . . . . . . . . . . 51
3.1.1 Impossibility result . . . . . . . . . . . . . . . . . . . . . . . . 52
3.1.2 Analysis of candidate definitions . . . . . . . . . . . . . . . . 54
3.1.3 Summary and discussion . . . . . . . . . . . . . . . . . . . . . 66
3.2 Defining Prime Implicates and Prime Implicants in Kn . . . . . . . . 67
3.2.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . 67
3.2.2 Desirable properties . . . . . . . . . . . . . . . . . . . . . . . 68
3.2.3 Analysis of candidate definitions . . . . . . . . . . . . . . . . 69
4 Generating and Recognizing Prime Implicates 79
4.1 Prime Implicate Generation . . . . . . . . . . . . . . . . . . . . . . . 79
4.1.1 Prime implicate generation in propositional logic . . . . . . . 79
4.1.2 The algorithm GenPI . . . . . . . . . . . . . . . . . . . . . . 80
4.1.3 Correctness of GenPI . . . . . . . . . . . . . . . . . . . . . . 82
4.1.4 Bounds on prime implicate size . . . . . . . . . . . . . . . . . 85
4.1.5 Bounds on the number of prime implicates . . . . . . . . . . 92
4.1.6 Improving the efficiency of GenPI . . . . . . . . . . . . . . . 95
4.2 Prime Implicate Recognition . . . . . . . . . . . . . . . . . . . . . . 100
4.2.1 Lower bound . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
4.2.2 Na¨ıve approach . . . . . . . . . . . . . . . . . . . . . . . . . . 100
4.2.3 Decomposition theorem . . . . . . . . . . . . . . . . . . . . . 101
4.2.4 Prime implicate recognition for propositional clauses . . . . . 106
4.2.5 Prime implicate recognition for 2-formulae . . . . . . . . . . 107
4.2.6 Prime implicate recognition for 3-formulae . . . . . . . . . . 108
4.2.7 The algorithm TestPI . . . . . . . . . . . . . . . . . . . . . . 113
5 Restricted Consequence Finding 119
5.1 New prime implicates . . . . . . . . . . . . . . . . . . . . . . . . . . 119
5.1.1 Properties of new prime implicates . . . . . . . . . . . . . . . 120
5.1.2 Generating and recognizing new prime implicates . . . . . . . 122
5.2 Signature-bounded prime implicates . . . . . . . . . . . . . . . . . . 123
5.2.1 Properties of signature-bounded prime implicates . . . . . . . 124
5.2.2 Generating signature-bounded prime implicates . . . . . . . . 128
5.2.3 Recognizing signature-bounded prime implicates . . . . . . . 128
6 Prime Implicate Normal Form 131
6.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
6.2 Definition of Prime Implicate Normal Form . . . . . . . . . . . . . . 132
6.3 Properties of Prime Implicate Normal Form . . . . . . . . . . . . . . 135
6.3.1 Tractable entailment . . . . . . . . . . . . . . . . . . . . . . . 135
6.3.2 Tractable uniform interpolation . . . . . . . . . . . . . . . . . 153
6.3.3 Canonicity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
6.4 Computing Prime Implicate Normal Form . . . . . . . . . . . . . . . 170
6.5 Spatial Complexity of Prime Implicate Normal Form . . . . . . . . . 173
6.6 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
6.6.1 Disjunctive form . . . . . . . . . . . . . . . . . . . . . . . . . 177
6.6.2 Linkless normal form . . . . . . . . . . . . . . . . . . . . . . . 179
7 Conclusion 183
A Complexity Theory 187
Bibliography 189
Index 197